[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification RGn-Decomp-Partial
enrich
   SPAWN, 
   RGn
with
   

   
   
   functions  Rton : nat → state × state → bool;
              Gton : nat → state × state → bool;
              Prton : nat → state → bool;
              Poton : nat → state → bool;
   
   
   variables  inpf : nat → input;
              outf : nat → output;
   
   

   

   axioms prton-def :  ⊦ Prton(n)(s) ↔ (∀ m. m ≤ n → Pr(m)(s));
          poton-def :  ⊦ Poton(n)(s) ↔ (∀ m. m ≤ n → Po(m)(s));
          rton-def :  ⊦ Rton(n)(s, s0) ↔ (∀ m. m ≤ n → Ry(m)(s, s0));
          gto-def :  ⊦ Gton(n)(s, s0) ↔ (∃ m. m ≤ n ∧ Gr(m)(s, s0));

   

   
end enrich